Lean 4でHello World
インストールはelanのページを見る
下のサンプルを参考にした方が良い。
code:memo
PS C:\Users\alles\workspace\ghworkspace\language\lean\my-lean-proj> lake build
error: dependency mathlib of myleanproj not in manifest, use lake update to update
PS C:\Users\alles\workspace\ghworkspace\language\lean\my-lean-proj> lake update
code:memo
lake build
stdout:
Hello, world!
"4.0.0-nightly-2023-06-08"
============================
lakeリポジトリのページに沿ってやったら普通にできた。
メモ